/*
Copyright 2007 Laura Giordano, Valentina Gliozzi, Gian Luca Pozzato

    This file is part of KLMLean.

    KLMLean is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    KLMLean is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with KLMLean.  If not, see <http://www.gnu.org/licenses/>.
*/


/* Theorem prover for KLM cumulative logic C */
:- op(400,fy,neg), 
   op(400,fy,box),
   op(400,fy,l),
   op(500,xfy,and), 
   op(600,xfy,or),
   op(650,xfy,->), 
   op(650,xfy,=>).
:-use_module(library(lists)).
:-use_module(library(ordsets)).


/* --------------------------------------------------------------------------------------- */

/* The following predicate implements the calculi:

    prove(Gamma,[],Tree,Analyzed) iff there exists a closed tableaux Tree for Gamma;\emptyset
    
*/

prove(Gamma,Sigma,Tree,Analyzed):-
  append(Gamma,Sigma,Node),
  list_to_ord_set(Node,Current),
  \+ord_member(Current,Analyzed),
  ord_add_element(Analyzed,Current,NewAnalyzed),
  proveStandard(Gamma,Sigma,Tree,NewAnalyzed).

  
proveStandard(Gamma,_,tree(ax,F),_):-
  member(neg F,Gamma),member(F, Gamma),!.

proveStandard(Gamma,Sigma,tree(andP,F,G,ST),Analyzed):-                                      
  select(F and G,Gamma,NewGamma),!,
  prove([F|[G|NewGamma]],Sigma,ST,Analyzed).

proveStandard(Gamma,Sigma,tree(orN,F,G,ST),Analyzed):-
  select(neg (F or G),Gamma,NewGamma),!,
  prove([neg F|[neg G|NewGamma]],Sigma,ST,Analyzed).


proveStandard(Gamma,Sigma,tree(impN,F,G,ST),Analyzed):-
  select(neg (F -> G),Gamma,NewGamma),!,
  prove([F|[neg G|NewGamma]],Sigma,ST,Analyzed).

proveStandard(Gamma,Sigma,tree(neg,F,ST),Analyzed):-
  select(neg neg F,Gamma,NewGamma),!,              
  prove([F|NewGamma],Sigma,ST,Analyzed).

proveStandard(Gamma,Sigma,tree(andN,F,G,ST1,ST2),Analyzed):-
  select(neg (F and G),Gamma,NewGamma),!,
  prove([neg F|NewGamma],Sigma,ST1,Analyzed),!,
  prove([neg G|NewGamma],Sigma,ST2,Analyzed).

proveStandard(Gamma,Sigma,tree(orP,F,G,ST1,ST2),Analyzed):-
  select(F or G,Gamma,NewGamma),!,
  prove([F|NewGamma],Sigma,ST1,Analyzed),!,
  prove([G|NewGamma],Sigma,ST2,Analyzed).
     
proveStandard(Gamma,Sigma,tree(impP,F,G,ST1,ST2),Analyzed):-
  select(F -> G,Gamma,NewGamma),!,
  prove([neg F|NewGamma],Sigma,ST1,Analyzed),!,
  prove([G|NewGamma],Sigma,ST2,Analyzed).
   
proveStandard(Gamma,Sigma,tree(entN,A,B,ST),Analyzed):-
  select(neg (A => B),Gamma,NewGamma),
  conditionals(NewGamma,CondGamma),                                  
  append(Sigma,CondGamma,DefGamma),
  prove([l A|[box neg l A|[neg l B|DefGamma]]],[],ST,Analyzed).
            

/* Remark: as a difference from the rule (|~+) presented in the papers, having 3 conclusions,  
   KLMLean 2.0 implements an equivalent one having only two conclusions: 
   
        \Gamma, A |~ B 						\Gamma, A |~ B
    -------------------------------------		  ---------------------------------------------
      (1) \Gamma, A |~ B, ~LA	           	            (1) ..., A |~ B, LA, []~LA
      (2) ..., A |~ B, LA, []~LA	        	    (2) \Gamma, A |~ B, LA -> (LA & []~LA & LB)
      (3) \Gamma, A |~ B, LA, []~LA, LB

   This chioce has been made in order to simplify the graphical user interface, displaying 
   only binary trees.

*/
proveStandard(Gamma,Sigma,tree(entP,A,B,ST1,ST2),Analyzed):-
  select(A => B,Gamma,NewGamma),
  conditionals(NewGamma,Cond),
  inboxed(NewGamma,InBoxed),
  append(Cond,InBoxed,Gammastar),
  append(Gammastar,Sigma,DefGammaLeft),
  prove([box neg l A|[l A|[A => B|DefGammaLeft]]],[],ST1,Analyzed),
  prove([(l A) -> (l A and box neg l A and l B)|NewGamma],[A => B|Sigma],ST2,Analyzed).

proveStandard(Gamma,_,tree(elleN,A,ST),Analyzed):-
  select(neg l A,Gamma,NewGamma),
  inelle(NewGamma,DefGamma),
  prove([neg A|DefGamma],[],ST,Analyzed).                                       

proveStandard(Gamma,_,tree(elleN,ST),Analyzed):-
  inelle(Gamma,DefGamma),
  prove(DefGamma,[],ST,Analyzed).                                       
                                       
/* Auxiliary predicates */

inelle([],[]):-!.
inelle([l A|Tail],[A|ResTail]):-!,inelle(Tail,ResTail).
inelle([_|Tail],ResTail):-!,inelle(Tail,ResTail).

conditionals([],[]):-!.
conditionals([A => B|Tail],[A => B|CondTail]):-!,conditionals(Tail,CondTail).
conditionals([neg (A => B)|Tail],[neg (A => B)|CondTail]):-!,conditionals(Tail,CondTail).
conditionals([_|Tail],CondTail):-conditionals(Tail,CondTail).
        
inboxed([],[]):-!.
inboxed([box A|Tail],[A|InBoxTail]):-!,inboxed(Tail,InBoxTail).
inboxed([_|Tail],InBoxTail):-inboxed(Tail,InBoxTail).


/* Predicate used to control that the inserted formula belongs to the language LC of C logic:

  - propositional formulas belong to LC
  - if A and B are propositionals, then A => B belongs to LC
  - a boolean combination F of formulas of LC belongs to LC
  
*/

parseinput([]):-!.
parseinput([F|Tail]):-parse(F),parseinput(Tail).

parse(P):-atom(P).
parse(F and G):-parse(F),parse(G).
parse(F or G):-parse(F),parse(G).
parse(F -> G):-parse(F),parse(G).
parse(neg F):-parse(F).
parse(A => B):-boolcomb(A),boolcomb(B).

boolcomb(P):-atom(P).
boolcomb(A and B):-boolcomb(A),boolcomb(B).
boolcomb(A or B):-boolcomb(A),boolcomb(B).
boolcomb(A -> B):-boolcomb(A),boolcomb(B).
boolcomb(neg A):-boolcomb(A).


/* Predicates used to reconstruct the proof tree (used by the GUI) */
javaTree(tree(ax,_),Node,jT(ax,Node,null,null)):-!.

javaTree(tree(andP,A,B,Sub),Node,jT(andP,Node,SubJava,null)):-!,
  select(A and B,Node,Temp),
  javaTree(Sub,[A|[B|Temp]],SubJava).
  
javaTree(tree(andN,A,B,S1,S2),Node,jT(andN,Node,SJ1,SJ2)):-!,
  select(neg (A and B),Node,Temp),
  javaTree(S1,[neg A|Temp],SJ1),
  javaTree(S2,[neg B|Temp],SJ2).  
  
javaTree(tree(orP,A,B,S1,S2),Node,jT(orP,Node,SJ1,SJ2)):-!,
  select(A or B,Node,Temp),
  javaTree(S1,[A|Temp],SJ1),  
  javaTree(S2,[B|Temp],SJ2).
  
javaTree(tree(orN,A,B,Sub),Node,jT(orN,Node,SubJava,null)):-!, 
  select(neg (A or B),Node,Temp), 
  javaTree(Sub,[neg A|[neg B|Temp]],SubJava).
  
javaTree(tree(impP,A,B,S1,S2),Node,jT(impP,Node,SJ1,SJ2)):-!,
  select(A -> B,Node,Temp),
  javaTree(S1,[neg A|Temp],SJ1),
  javaTree(S2,[B|Temp],SJ2).
 
javaTree(tree(neg,A,Sub),Node,jT(neg,Node,SubJava,null)):-!,
  select(neg neg A,Node,Temp),
  javaTree(Sub,[A|Temp],SubJava).

javaTree(tree(impN,A,B,Sub),Node,jT(impN,Node,SubJava,null)):-!,   
  select(neg (A -> B),Node,Temp),
  javaTree(Sub,[A|[neg B|Temp]],SubJava).
  
javaTree(tree(entP,A,B,S1,S2),Node,jT(entP,Node,SJ1,SJ2)):-!,
  conditionals(Node,Cond), 
  inboxed(Node,InBoxed),
  append(Cond,InBoxed,DefGammaLeft),
  javaTree(S1,[box neg l A|[l A|[A => B|DefGammaLeft]]],SJ1),
  javaTree(S2,[(l A) -> (l A and box neg l A and l B)|Node],SJ2).  
  
javaTree(tree(entN,A,B,Sub),Node,jT(entN,Node,SubJava,null)):-!,  
  select(neg (A => B),Node,Temp),
  conditionals(Temp,Cond),
  javaTree(Sub,[l A|[box neg l A|[neg l B|Cond]]],SubJava).  
  

javaTree(tree(elleN,A,Sub),Node,jT(elleN,Node,SubJava,null)):-!,
  select(neg l A,Node,Temp),
  inelle(Temp,Def),
  javaTree(Sub,[neg A|Def],SubJava).
  
javaTree(tree(elleN,Sub),Node,jT(elleN,Node,SubJava,null)):-!,  
  inelle(Node,Temp),
  javaTree(Sub,Temp,SubJava).
                                     

/* Predicates used by the GUI to extract information about the closed tree */

getRule(jT(Rule,_,_,_),Rule):-!.
getNode(jT(_,Node,_,_),Node):-!.
getLeft(jT(_,_,Left,_),Left):-!.
getRight(jT(_,_,_,Right),Right):-!.


/* Top-level predicates */
unsat(Gamma,Tree):-parseinput(Gamma),prove(Gamma,[],Tree,[]).
nmcr(K,F,Tree):-parseinput([F|K]),prove([neg F|K],[],Tree,[]).
unsatinterface(K,[F],Tree):-prove([neg F|K],[],Tree,[]).
unsatinterface(K,[],Tree):-prove(K,[],Tree,[]).